Inference at * 2 2 1 1 1 
Iof proof for Lemma p-fun-exp-add-sq:



1. A : Type
2. f : A(A + Top)
3. x : A
4. m : 
5. 0 < m
6. n:. (can-apply(f^m - 1;x))  ((f^n+(m - 1)(x)) ~ (f^n(do-apply(f^m - 1;x))))
7. n : 
8. can-apply(f^m;x)
9. (n = 0)
10. (n+m = 0)
11. (n = 0)
12. (m = 0)
  can-apply(f^m - 1;x) 

latex

 by (Using [`n',m] (BLemma `can-apply-fun-exp`) ) 
CollapseTHEN (Auto) 

latex

C.

Definitions	t  T, , {x:A| B(x)} , x:A. B(x), A  B, A, False, P  Q, x:AB(x), Void, a < b, n - m, n+m, -n
Lemmas	can-apply-fun-exp